Library midpoint
Require Export PointsETC.
Require Import incidence.
Section Triangle.
Context `{M:triangle_theory}.
Definition midpoint P U :=
match P,U with
cTriple p q r, cTriple u v w ⇒
let h := a×p+b×q+c×r in
let k := a×u+b×v+c×w in
cTriple (k×p + h×u) (k×q + h×v) (k×r + h×w)
end.
Lemma midpoint_col : ∀ A B,
col A B (midpoint A B).
Proof.
intros.
destruct A;destruct B.
simpl.
unfold col;simpl.
ring.
Qed.
Lemma X5_is_midpoint_of_X3_X4 :
eq_points X_5 (midpoint X_3 X_4).
Proof.
intros.
red;simpl; repeat split; field; repeat split;try assumption.
Qed.
End Triangle.
Require Import incidence.
Section Triangle.
Context `{M:triangle_theory}.
Definition midpoint P U :=
match P,U with
cTriple p q r, cTriple u v w ⇒
let h := a×p+b×q+c×r in
let k := a×u+b×v+c×w in
cTriple (k×p + h×u) (k×q + h×v) (k×r + h×w)
end.
Lemma midpoint_col : ∀ A B,
col A B (midpoint A B).
Proof.
intros.
destruct A;destruct B.
simpl.
unfold col;simpl.
ring.
Qed.
Lemma X5_is_midpoint_of_X3_X4 :
eq_points X_5 (midpoint X_3 X_4).
Proof.
intros.
red;simpl; repeat split; field; repeat split;try assumption.
Qed.
End Triangle.